Inference at * 1 
Iof proof for Lemma fseg extend:



1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1)
7. ||l1|| < ||l2||
8. l2[(||l2|| - (||l1||+1))] = v
9. (null(L))
10. L':T List. (L = (L' @ [last(L)]))
  L@0:T List. ((L @ l1) = (L@0 @ [v / l1])) 

latex

 by ((((ParallelOp ( -1)) 
CollapseTHEN (((((if (first_bool T:b
C) then HypSubst' else RevHypSubst') ( -1)( 0))) 
CollapseTHEN (Auto))))) 
CollapseTHEN (((
CRWO "append_assoc" 0) 
CollapseTHENA (Auto)))) 

latex

C1: 

C1: 10. L' : T List
C1: 11. L = (L' @ [last(L)])
C1:   (L' @ [last(L)] @ l1) = (L' @ [v / l1])
C.

Definitions	x:A. B(x), i  j , A  B, SQType(T), {T}, s ~ t, , S  T, Top, x:A.B(x), Void, {x:A| B(x)} , , , P  Q, P & Q, x:A  B(x), P  Q, P  Q, last(L), [], l[i], n - m, n+m, ||as||, #$n, A, a < b, Type, as @ bs, [car / cdr], x:A. B(x), x:AB(x), s = t, A List, type List, t  T
Lemmas	non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, member wf, iff wf, rev implies wf, append assoc, last wf, append wf